The source code of this example can be downloaded here.

A modle language Simplified CSP (SCSP), which is a small subset of CSP, is used as a running example for the purpose of illustration. In SCSP, a process is constructed only by event prefixing or interleaving. The syntax of SCSP is as follows:

P = e -> P | P ||| P |  Skip;

(A). Generate Code with Module Generator

With the Module Generator, it is very convenient and simple to generate the code for a SCSP model checker as illustrated by the following figure.

Once the code generation is completed, the following dialogue will appear to inform you.

Now you can open the Windows Explorer to locate the generated C# project:

(B). Complete the generated code

Double click PAT3 Source.sln and you will open the C# solution in Microsoft Visual Studio.

In the generated solution, there are two projects:

• PAT.Main, contains the interface to the GUI package of PAT; one can refine the GUI editor for the language by re-implementing the class EditorTabItem.cs, and re-organizing error messages by modifying ErrorListWindow.cs.
  Note: no modification is required here, unless one want to re-implement the editor.
• PAT.Module.SCSP, contains the code for all the rest stuffs, as follows:
  • Assertions: this folder provides model checking for deadlock and state reachability checking, recalling that in part (A) only these two kinds of assertions are chosen to be supported. Thus, the parser should support the syntax for these two types of assertions, too. In the generated code, the default model checking algorithms of PAT are inherited, and developers can re-implement the algorithms by him/herself.
    
  • LTS: this folder contains two catergories of functionality. The first is to provide a parser to analyze a SCSP model, and the second is to describe each language construct as a class and integrate the semantics of each language construct into the method MoveOneStep.
    Note that the parser classes are not generated automatically. Thus, one needs to create parser classes manually, e.g., SCSPTreeLexer.cs, SCSPTreeParser.cs, and SCSPTreeWalker.cs.
    Besides, there are two classes that are created for specific purposes.
    
    • Configuration.cs, the class the represents the semantic model of your language. By default, the code is complete and you need not modify anything.
    • Specification.cs, the controlling class, which communicates with ModuleFascade.cs and LTS. Two methods are important and should be completed in order to make the code effects, and they are:
      1. ParseSpec(): code should be added here to invoke the parser to analyze the input model. Note that this method will be invoked before each request of simulation or verification. Meanwhile, also make sure that each assertion has been initialized within this method, by code like the following:
         
      2. SimulationInitialization(): code should be added here to generate the model list (at least one model) that will appear in the simulator window, once simulation button is clicked. Note that if this method is not implemented, the simulatior would not function properly.
    The rest of classes in LTS are all language construct representations, including Definition, DefinitionRef, EventPrefix, Interleave, Process, Skip and Stop. Make sure that proper instances are created by the parser based on a certain input model.